perm filename BLIROB.COM[226,JMC] blob
sn#005387 filedate 1972-06-03 generic text, type T, neo UTF8
00100 (GIVEAX EQ1 ((FORALL X) (EQUAL X X)))
00200 (GIVEAX
00300 EQ2
00400 ((FORALL X)
00500 ((FORALL Y) (IMPLIES (EQUAL X Y) (EQUAL Y X)))))
00600 (GIVEAX
00700 EQ3
00800 ((FORALL X)
00900 ((FORALL Y)
01000 ((FORALL Z)
01100 (IMPLIES
01200 (AND (EQUAL X Y) (EQUAL Y Z))
01300 (EQUAL X Z))))))
01400 (GIVEAX
01500 TABLEEMPTY
01600 ((FORALL X)
01700 (IMPLIES
01800 (AND (NOT (EQUAL X ROBOT)) (NOT (HOLDING X S0)))
01900 (NOT (AT X TABLE S0)))))
02000 (GIVEAX
02100 DIFFOBJ
02200 (AND
02300 (NOT (EQUAL BOX1 BOX2))
02400 (AND
02500 (NOT (EQUAL BOX1 TABLE))
02600 (AND
02700 (NOT (EQUAL BOX1 DOOR))
02800 (AND
02900 (NOT (EQUAL BOX1 OUTSIDE))
03000 (AND
03100 (NOT (EQUAL BOX2 TABLE))
03200 (AND
03300 (NOT (EQUAL BOX2 DOOR))
03400 (AND
03500 (NOT (EQUAL BOX2 OUTSIDE))
03600 (AND
03700 (NOT (EQUAL TABLE DOOR))
03800 (AND
03900 (NOT (EQUAL TABLE OUTSIDE))
04000 (NOT (EQUAL DOOR OUTSIDE))))))))))))
04100 (GIVEAX
04200 ATONE
04300 ((FORALL X)
04400 ((FORALL P1)
04500 ((FORALL P2)
04600 ((FORALL S)
04700 (IMPLIES
04800 (AND (AT X P1 S) (AT X P2 S))
04900 (EQUAL P1 P2)))))))
05000 (GIVEAX
05100 REDDOOR
05200 ((THEREEXISTS X)
05300 (AND
05400 (RED X)
05500 (AND
05600 (NOT (EQUAL X ROBOT))
05700 (AND
05800 (AT X DOOR S0)
05900 ((FORALL Y)
06000 (IMPLIES
06100 (AND
06200 (AT Y DOOR S0)
06300 (AND
06400 (NOT (EQUAL Y ROBOT))
06500 (NOT (HOLDING Y S0))))
06600 (RED Y))))))))
06700 (GIVEAX
06800 ISKEYBOX
06900 (OR (EQUAL KEYBOX BOX1) (EQUAL KEYBOX BOX2)))
07000 (GIVEAX
07100 KEYBOX1
07200 ((THEREEXISTS X)
07300 (AND
07400 (KEY X)
07500 (AND
07600 (NOT (EQUAL X ROBOT))
07700 (AND (AT X KEYBOX S0) (NOT (HOLDING X S0)))))))
07800 (GIVEAX
07900 KEYBOX2
08000 ((FORALL Y)
08100 (IMPLIES
08200 (AND
08300 (AT Y KEYBOX S0)
08400 (AND (NOT (EQUAL Y ROBOT)) (NOT (HOLDING Y S0))))
08500 (KEY Y))))
08600 (GIVEAX B1B2 (NOT (EQUAL BOX1 BOX2)))
08700 (GIVEAX B1T (NOT (EQUAL BOX1 TABLE)))
08800 (GIVEAX B1D (NOT (EQUAL BOX1 DOOR)))
08900 (GIVEAX B1O (NOT (EQUAL BOX1 OUTSIDE)))
09000 (GIVEAX B2T (NOT (EQUAL BOX2 TABLE)))
09100 (GIVEAX B2D (NOT (EQUAL BOX2 DOOR)))
09200 (GIVEAX B2O (NOT (EQUAL BOX2 OUTSIDE)))
09300 (GIVEAX TD (NOT (EQUAL TABLE DOOR)))
09400 (GIVEAX TO (NOT (EQUAL TABLE OUTSIDE)))
09500 (GIVEAX DO (NOT (EQUAL DOOR OUTSIDE)))
09600 (GIVEAX
09700 HOLDING
09800 ((FORALL S)
09900 ((FORALL X)
10000 ((FORALL Y)
10100 (IMPLIES
10200 (AND (AT ROBOT Y S) (HOLDING X S))
10300 (AT X Y S))))))
10400 (GIVEAX
10500 HOLD2
10600 ((FORALL S)
10700 ((FORALL X)
10800 ((FORALL Y)
10900 (IMPLIES
11000 (AND (HOLDING X S) (HOLDING Y S))
11100 (EQUAL X Y))))))
11200 (GIVEAX
11300 PICKUP
11400 ((FORALL S)
11500 ((AND
11600 ((LAMBDA SP)
11700 ((FORALL X)
11800 ((FORALL Y) (EQUIVALENT (AT X Y S) (AT X Y SP)))))
11900 ((FORALL Z)
12000 (IMPLIES
12100 (AND
12200 (AT ROBOT Z S)
12300 ((THEREEXISTS X)
12400 (AND (NOT (EQUAL X ROBOT)) (AT X Z S))))
12500 ((THEREEXISTS X) (HOLDING X SP)))))
12600 (PICKUP S))))
12700 (GIVEAX
12800 GO1
12900 ((FORALL S)
13000 ((FORALL Z)
13100 ((FORALL W)
13200 (EQUIVALENT (HOLDING W S) (HOLDING W (GOO Z S)))))))
13300 (GIVEAX
13400 GO2
13500 ((FORALL S)
13600 ((FORALL Z)
13700 (IMPLIES
13800 (OR
13900 (NOT (EQUAL Z OUTSIDE))
14000 ((THEREEXISTS X) (AND (AT X DOOR S) (KEY X))))
14100 (AT ROBOT Z (GOO Z S))))))
14200 (GIVEAX
14300 GO3
14400 ((FORALL S)
14500 ((FORALL Z)
14600 ((FORALL X)
14700 ((FORALL Y)
14800 (IMPLIES
14900 (AND
15000 (AT X Y S)
15100 (AND (NOT (EQUAL X ROBOT)) (NOT (HOLDING X S))))
15200 (AT X Y (GOO Z S))))))))
15300 (GIVEAX
15400 GO4
15500 (IMPLIES
15600 (AND
15700 ((FORALL S)
15800 ((FORALL Y)
15900 ((FORALL X) (NOT (AND (AT X DOOR S) (KEY X))))))
16000 (AT ROBOT Y S))
16100 (AT ROBOT Y (GOO OUTSIDE S))))
16200 (GIVEAX
16300 GO5
16400 ((FORALL S)
16500 ((FORALL Z)
16600 ((FORALL X)
16700 ((FORALL Y)
16800 (IMPLIES
16900 (AND
17000 (NOT (EQUAL X ROBOT))
17100 (AND (NOT (HOLDING X S)) (AT X Y (GOO Z S))))
17200 (AT X Y S)))))))
17300 (GIVEAX
17400 RELEASE1
17500 ((FORALL S)
17600 ((FORALL X)
17700 ((FORALL Y)
17800 (EQUIVALENT (AT X Y S) (AT X Y (RELEASE S)))))))
17900 (GIVEAX
18000 RELEASE2
18100 ((FORALL S)
18200 ((FORALL X) (NOT (HOLDING X (RELEASE S))))))
18300 (PROOF ONE)
18400 1 (ASS (EQUAL S1 (GOO TABLE S0)))
18500 2 (USEAX GO2 S0 TABLE)
18600 3 (USEAX TO)
18700 4 (OI
18800 3
18900 ((THEREEXISTS X) (AND (AT X DOOR S0) (KEY X))))
19000 5 (MP 2 4)
19100 6 (REPR 5 1 1)
19200 7 (USEAX GO3 S0 TABLE X Y)
19300 8 (REPR 7 1 1)
19400 9 (USEAX REDDOOR R)
19500 10 (USEAX GO3 S0 TABLE R DOOR)
19600 11 (ASS (NOT (HOLDING R S0)))
19700 12 (AE 9 1)
19800 13 (AE 9 2)
19900 14 (AE 13 1)
20000 15 (AE 13 2)
20100 16 (AE 15 1)
20200 17 (AE 15 2)
20300 18 (AI 14 11)
20400 19 (AI 16 18)
20500 20 (MP 10 19)
20600 21 (REPR 20 1 1)
20700 22 (USEAX KEYBOX1 K)
20800 23 (AE 22 1)
20900 24 (AE 22 2)
21000 25 (AE 24 1)
21100 26 (AE 24 2)
21200 27 (AE 26 1)
21300 28 (AE 26 2)
21400 29 (USEAX GO3 S0 TABLE K KEYBOX)
21500 30 (AI 25 28)
21600 31 (AI 27 30)
21700 32 (MP 31 29)
21800 33 (REPR 32 1 1)
21900 34 (USEAX GO1 S0 TABLE K)
22000 35 (EQE 34 2)
22100 36 (REPR 35 1 1)
22200 37 (ASS (HOLDING K S1))
22300 38 (MP 37 36)
22400 39 (ASS TRUE)
22500 40 (NE 28 38)
22600 41 (DED 40 37)
22700 42 (NI 41)
22800 43 (AI 23 33)
22900 44 (EG 43 K)
23000 45 (ASS (AT Y KEYBOX S1))
23100 46 (ASS (EQUAL Y ROBOT))
23200 47 (REPL 45 46 1)
23300 48 (USEAX ATONE ROBOT KEYBOX TABLE S1)
23400 49 (AI 47 6)
23500 50 (MP 48 49)
23600 51 (USEAX ISKEYBOX)
23700 52 (REPL 51 50 1)
23800 53 (REPL 52 50 1)
23900 54 (USEAX B1T)
24000 55 (USEAX B2T)
24100 56 (ASS (EQUAL TABLE BOX1))
24200 57 (USEAX EQ2 TABLE BOX1)
24300 58 (MP 56 57)
24400 59 (NE 54 58)
24500 60 (DED 59 56)
24600 61 (ASS (EQUAL TABLE BOX2))
24700 62 (USEAX EQ2 TABLE BOX2)
24800 63 (MP 62 61)
24900 64 (NE 63 55)
25000 65 (DED 64 61)
25100 66 (OE 53 60 65)
25200 67 (DED 66 46)
25300 68 (NI 67)
25400 69 (ASS (HOLDING Y S0))
25500 70 (USEAX GO1 S0 TABLE Y)
25600 71 (EQE 70 1)
25700 72 (MP 71 69)
25800 73 (REPR 72 1 1)
25900 74 (USEAX HOLDING S1 Y TABLE)
26000 75 (AI 6 73)
26100 76 (MP 74 75)
26200 77 (USEAX ATONE Y KEYBOX TABLE S1)
26300 78 (AI 45 76)
26400 79 (MP 77 78)
26500 80 (USEAX ISKEYBOX)
26600 81 (ASS (EQUAL KEYBOX BOX1))
26700 82 (REPL 79 81 1)
26800 83 (USEAX B1T)
26900 84 (NE 82 83)
27000 85 (DED 84 81)
27100 86 (ASS (EQUAL KEYBOX BOX2))
27200 87 (REPL 79 86 1)
27300 88 (USEAX B2T)
27400 89 (NE 87 88)
27500 90 (DED 89 86)
27600 91 (OE 80 85 90)
27700 92 (DED 91 69)
27800 93 (NI 92)
27900 94 (AI 68 93)
28000 95 (USEAX GO5 S0 TABLE Y KEYBOX)
28100 96 (REPR 95 1 1)
28200 97 (AI 93 45)
28300 98 (AI 68 97)
28400 99 (MP 96 98)
28500 100 (AI 99 94)
28600 101 (USEAX KEYBOX2 Y)
28700 102 (MP 100 101)
28800 103 (DED 102 45)
28900 104 (UG 103 Y)
29000 105 (ASS (AT X Y (GOO Z S)))
29100 106 (ASS (NOT (EQUAL Z Y)))
29200 107 (ASS
29300 (OR
29400 (NOT (EQUAL Z OUTSIDE))
29500 ((THEREEXISTS X)
29600 (AND (AT X DOOR S) (KEY X)))))
29700 108 (ASS (EQUAL X ROBOT))
29800 109 (USEAX GO2 S Z)
29900 110 (MP 107 109)
30000 111 (REPR 110 108 1)
30100 112 (USEAX ATONE X Y Z (GOO Z S))
30200 113 (AI 105 111)
30300 114 (MP 112 113)
30400 115 (REPR 106 114 1)
30500 116 (USEAX EQ1 Y)
30600 117 (NE 115 116)
30700 118 (DED 117 108)
30800 119 (NI 118)
30900 120 (ASS (HOLDING X S))
31000 121 (USEAX GO1 S Z X)
31100 122 (TAUT (HOLDING X (GOO Z S)) 120 121)
31200 123 (USEAX HOLDING (GOO Z S) X Z)
31300 124 (AI 110 122)
31400 125 (MP 124 123)
31500 126 (AI 125 105)
31600 127 (USEAX ATONE X Z Y (GOO Z S))
31700 128 (MP 126 127)
31800 129 (NE 128 106)
31900 130 (DED 129 120)
32000 131 (NI 130)
32100 132 (USEAX GO5 S Z X Y)
32200 133 (AI 131 105)
32300 134 (AI 119 133)
32400 135 (MP 134 132)
32500 136 (DED 135 107)
32600 137 (DED 136 106)
32700 138 (DED 137 105)
32800 139 (UG 138 X Y Z S)
32900 140 (ASS (AT X DOOR S1))
33000 141 (US 139 S0 TABLE DOOR X)
33100 142 (USEAX TD)
33200 143 (USEAX TO)
33300 144 (REPL 140 1 1)
33400 145 (MP 144 141)
33500 146 (MP 145 142)
33600 147 (OI
33700 143
33800 ((THEREEXISTS X1)
33900 (AND (AT X1 DOOR S0) (KEY X1))))
34000 148 (MP 147 146)
34100 149 (USEAX REDDOOR)
34200 150 (ES 149 R1)
34300 151 (AE 150 2)
34400 152 (AE 151 2)
34500 153 (AE 152 2)
34600 154 (US 153 X)
34700 155 (ASS (HOLDING X S0))
34800 156 (USEAX GO1 S0 TABLE X)
34900 157 (TAUT (HOLDING X (GOO TABLE S0)) 155 156)
35000 158 (REPR 157 1 1)
35100 159 (USEAX HOLDING S1 X TABLE)
35200 160 (AI 6 158)
35300 161 (MP 160 159)
35400 162 (USEAX ATONE X DOOR TABLE S1)
35500 163 (AI 140 161)
35600 164 (MP 163 162)
35700 165 (USEAX TD)
35800 166 (REPL 165 164 1)
35900 167 (USEAX EQ1 TABLE)
36000 168 (NE 166 167)
36100 169 (DED 168 155)
36200 170 (NI 169)
36300 171 (ASS (EQUAL X ROBOT))
36400 172 (REPR 6 171 1)
36500 173 (USEAX ATONE X DOOR TABLE S1)
36600 174 (AI 140 172)
36700 175 (MP 174 173)
36800 176 (USEAX TD)
36900 177 (REPR 176 175 1)
37000 178 (USEAX EQ1 DOOR)
37100 179 (NE 177 178)
37200 180 (DED 179 171)
37300 181 (NI 180)
37400 182 (AI 181 170)
37500 183 (AI 148 182)
37600 184 (MP 183 154)
37700 185 (DED 184 140)
37800 186 (UG 185 X)
37900 187 (ASS (AT U KEYBOX S1))
38000 188 (REPL 187 1 1)
38100 189 (US 139 S0 TABLE KEYBOX U)
38200 190 (MP 189 188)
38300 191 (ASS (EQUAL TABLE KEYBOX))
38400 192 (USEAX ISKEYBOX)
38500 193 (ASS (EQUAL KEYBOX BOX1))
38600 194 (REPL 191 193 1)
38700 195 (USEAX B1T)
38800 196 (REPL 195 194 1)
38900 197 (USEAX EQ1 BOX1)
39000 198 (NE 196 197)
39100 199 (DED 198 193)
39200 200 (ASS (EQUAL KEYBOX BOX2))
39300 201 (REPL 191 200 1)
39400 202 (USEAX B2T)
39500 203 (REPL 202 201 1)
39600 204 (USEAX EQ1 BOX2)
39700 205 (NE 203 204)
39800 206 (DED 205 200)
39900 207 (OE 192 199 206)
40000 208 (DED 207 191)
40100 209 (NI 208)
40200 210 (MP 190 209)
40300 211 (USEAX TO)
40400 212 (OI
40500 211
40600 ((THEREEXISTS X) (AND (AT U DOOR S0) (KEY U))))
40700 213 (MP 212 210)
40800 214 (ASS (HOLDING U S0))
40900 215 (USEAX GO1 S0 TABLE U)
41000 216 (REPR 215 1 1)
41100 217 (EQE 216 1)
41200 218 (MP 217 214)
41300 219 (USEAX HOLDING S1 U TABLE)
41400 220 (AI 6 218)
41500 221 (MP 219 220)
41600 222 (USEAX ATONE U TABLE KEYBOX S1)
41700 223 (AI 221 187)
41800 224 (MP 223 222)
41900 225 (NE 224 209)
42000 226 (DED 225 214)
42100 227 (NI 226)